M.init(x,v) == x0 != (M.2.2).1(x)  v = x0 

latex

---

clarification:

M.init(x,v) == fpf-val(IdDeq; ((M.2.2).1); x; a,x0.(v = x0  fpf-cap(M.1;IdDeq;x;Void))) 

latex

Definitions	z != f(x)  P(a;z), t.2, s = t, x:AB(x), , f(x)?z, t.1, IdDeq, Void
FDL editor aliases	ma-init